
; Copyright (c) 2015 Microsoft Corporation

(set-option :produce-models true)
(declare-const p Bool)
(assert (not p))
(apply elim-uncnstr :print-model-converter true)
(reset)
(echo "-----")

(set-option :produce-models true)
(declare-const p1 Bool)
(declare-const p2 Bool)
(assert (not p1))
(assert (or p1 p2))
(assert (or p1 (not p2)))
(apply elim-uncnstr :print-model-converter true)
(reset)
(echo "-----")

(set-option :produce-models true)
(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-fun p (Bool) Bool)
(assert (p (and p1 p2)))
(apply elim-uncnstr :print-model-converter true)
(reset)
(echo "-----")

(set-option :produce-models true)
(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-fun p (Bool) Bool)
(assert (p (and p1 p2)))
(assert p1)
(apply elim-uncnstr :print-model-converter true)
(reset)
(echo "-----")

(set-option :produce-models true)
(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-fun p (Bool) Bool)
(assert (p (or p1 p2)))
(apply elim-uncnstr :print-model-converter true)
(reset)
(echo "-----")

(set-option :produce-models true)
(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-fun p (Bool) Bool)
(assert (p (or p1 p2)))
(assert p1)
(apply elim-uncnstr :print-model-converter true)
(reset)
(echo "-----")
